/*
 * PosCSParser.hpp
 *
 * Copyright 2013 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef POSCSPARSER_HPP_
#define POSCSPARSER_HPP_

#include <iostream>
#include <string>

#include <boost/lexical_cast.hpp>

#include "bfr/CSVector.hpp"

namespace bfr {

class PosCSParser {
    public:
        /**
         * The problem type defined in the problem line.
         */
        enum problem_type {
            CNF, /*!<CNF (conjunctive normal form) problem. */
            UNKNOWN /*!< Something else. */
        };

        PosCSParser();
        ~PosCSParser();

        /**
         * Returns the number of variables in the last parsed input.
         *
         * This method returns 0 if no DNF has been parsed yet.
         *
         * @return Number of variables in the last parsed input.
         */
        size_t getVariableCount() const;

        PosCS parse(std::istream &in, bool sortClause=true) throw(std::string);

         /**
          * The comment character ('c').
          */
         static const char COMMENT_CHAR;

         /**
          * The problem line character ('p').
          */
         static const char PROBLEM_CHAR;

         /**
          * Minus character ('-').
          */
         static const char MINUS;

         /**
          * CNF problem as string ("cnf").
          */
         static const char CNF_PROBLEM[];

    private:
        size_t variableCount;
        size_t clauseCount;
        PosCS clauses;
        problem_type type;

        void readProblemLine(std::string &line) throw(std::string);
        size_t parseNumber(std::string &line, size_t *pos) throw(std::string);
        void readClause(std::string &line, bool sort) throw(std::string);
        inline bool isLineEmpty(const std::string &line) const;
};

} /* namespace bfr */

#endif  // POSCSPARSER_HPP_
